

LEMMA

If ec(x,y) and po(y,z), then z is not part of x.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (po y z)) => (~ (p z x))))))


> revsk
=============================
Step 2

? (((~ (ec c424030 c424029)) v (~ (po c424029 c424028))) v (~ (p c424028 c424030)))


> hypdisj
=============================
Step 3

? (~ (p c424028 c424030))

1. (po c424029 c424028)
2. (ec c424030 c424029)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 4
|
|? (c Var70 c424028)
|
|1. (p c424028 c424030)
|2. (po c424029 c424028)
|3. (ec c424030 c424029)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 5
||
||? (p Var73 c424028)
||
||1. (~ (c Var70 c424028))
||2. (p c424028 c424030)
||3. (po c424029 c424028)
||4. (ec c424030 c424029)
||
||> ((p Z X) <-- (~ (c (f418977 Z X Y) Z)))
||=============================
||Step 6
||
||? (~ (c (f418977 Var73 c424028 Var76) Var73))
||
||1. (~ (p Var73 c424028))
||2. (~ (c Var70 c424028))
||3. (p c424028 c424030)
||4. (po c424029 c424028)
||5. (ec c424030 c424029)
||
||> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|||=============================
|||Step 7
|||
|||? (p (f418994 Var82 Var79) Var79)
|||
|||1. (c (f418977 (f418994 Var82 Var79) c424028 Var76) (f418994 Var82 Var79))
|||2. (~ (p (f418994 Var82 Var79) c424028))
|||3. (~ (c Var70 c424028))
|||4. (p c424028 c424030)
|||5. (po c424029 c424028)
|||6. (ec c424030 c424029)
|||
|||> ((p (f418994 X Y) Y) <-- (o X Y))
|||=============================
|||Step 8
|||
|||? (o Var82 Var79)
|||
|||1. (~ (p (f418994 Var82 Var79) Var79))
|||2. (c (f418977 (f418994 Var82 Var79) c424028 Var76) (f418994 Var82 Var79))
|||3. (~ (p (f418994 Var82 Var79) c424028))
|||4. (~ (c Var70 c424028))
|||5. (p c424028 c424030)
|||6. (po c424029 c424028)
|||7. (ec c424030 c424029)
|||
|||> ((o X Y) <-- (po X Y))
|||=============================
|||Step 9
|||
|||? (po Var82 Var79)
|||
|||1. (~ (o Var82 Var79))
|||2. (~ (p (f418994 Var82 Var79) Var79))
|||3. (c (f418977 (f418994 Var82 Var79) c424028 Var76) (f418994 Var82 Var79))
|||4. (~ (p (f418994 Var82 Var79) c424028))
|||5. (~ (c Var70 c424028))
|||6. (p c424028 c424030)
|||7. (po c424029 c424028)
|||8. (ec c424030 c424029)
|||
|||> hyp
||=============================
||Step 10
||
||? (~ (c (f418977 (f418994 c424029 c424028) c424028 Var76) c424028))
||
||1. (c (f418977 (f418994 c424029 c424028) c424028 Var76) (f418994 c424029 c424028))
||2. (~ (p (f418994 c424029 c424028) c424028))
||3. (~ (c Var70 c424028))
||4. (p c424028 c424030)
||5. (po c424029 c424028)
||6. (ec c424030 c424029)
||
||> ((~ (c (f418977 Y Z X) Z)) <-- (~ (p Y Z)))
||=============================
||Step 11
||
||? (~ (p (f418994 c424029 c424028) c424028))
||
||1. (c (f418977 (f418994 c424029 c424028) c424028 Var76) c424028)
||2. (c (f418977 (f418994 c424029 c424028) c424028 Var76) (f418994 c424029 c424028))
||3. (~ (p (f418994 c424029 c424028) c424028))
||4. (~ (c Var70 c424028))
||5. (p c424028 c424030)
||6. (po c424029 c424028)
||7. (ec c424030 c424029)
||
||> hyp
|=============================
|Step 12
|
|? (c (f418977 (f418994 c424029 c424028) Var93 Var94) (f418994 c424029 c424028))
|
|1. (~ (c (f418977 (f418994 c424029 c424028) Var93 Var94) c424028))
|2. (p c424028 c424030)
|3. (po c424029 c424028)
|4. (ec c424030 c424029)
|
|> ((c (f418977 Y Z X) Y) <-- (~ (p Y Z)))
|=============================
|Step 13
|
|? (~ (p (f418994 c424029 c424028) Var93))
|
|1. (~ (c (f418977 (f418994 c424029 c424028) Var93 Var94) (f418994 c424029 c424028)))
|2. (~ (c (f418977 (f418994 c424029 c424028) Var93 Var94) c424028))
|3. (p c424028 c424030)
|4. (po c424029 c424028)
|5. (ec c424030 c424029)
|
|> ((~ (p X Y)) <-- (p X Z) (~ (o Y Z)))
||=============================
||Step 14
||
||? (p (f418994 c424029 c424028) c424029)
||
||1. (p (f418994 c424029 c424028) Var93)
||2. (~ (c (f418977 (f418994 c424029 c424028) Var93 Var94) (f418994 c424029 c424028)))
||3. (~ (c (f418977 (f418994 c424029 c424028) Var93 Var94) c424028))
||4. (p c424028 c424030)
||5. (po c424029 c424028)
||6. (ec c424030 c424029)
||
||> ((p (f418994 X Y) X) <-- (o X Y))
||=============================
||Step 15
||
||? (o c424029 c424028)
||
||1. (~ (p (f418994 c424029 c424028) c424029))
||2. (p (f418994 c424029 c424028) Var93)
||3. (~ (c (f418977 (f418994 c424029 c424028) Var93 Var94) (f418994 c424029 c424028)))
||4. (~ (c (f418977 (f418994 c424029 c424028) Var93 Var94) c424028))
||5. (p c424028 c424030)
||6. (po c424029 c424028)
||7. (ec c424030 c424029)
||
||> ((o X Y) <-- (po X Y))
||=============================
||Step 16
||
||? (po c424029 c424028)
||
||1. (~ (o c424029 c424028))
||2. (~ (p (f418994 c424029 c424028) c424029))
||3. (p (f418994 c424029 c424028) Var93)
||4. (~ (c (f418977 (f418994 c424029 c424028) Var93 Var94) (f418994 c424029 c424028)))
||5. (~ (c (f418977 (f418994 c424029 c424028) Var93 Var94) c424028))
||6. (p c424028 c424030)
||7. (po c424029 c424028)
||8. (ec c424030 c424029)
||
||> hyp
|=============================
|Step 17
|
|? (~ (o Var93 c424029))
|
|1. (p (f418994 c424029 c424028) Var93)
|2. (~ (c (f418977 (f418994 c424029 c424028) Var93 Var94) (f418994 c424029 c424028)))
|3. (~ (c (f418977 (f418994 c424029 c424028) Var93 Var94) c424028))
|4. (p c424028 c424030)
|5. (po c424029 c424028)
|6. (ec c424030 c424029)
|
|> ((~ (o X Y)) <-- (ec X Y))
|=============================
|Step 18
|
|? (ec Var93 c424029)
|
|1. (o Var93 c424029)
|2. (p (f418994 c424029 c424028) Var93)
|3. (~ (c (f418977 (f418994 c424029 c424028) Var93 Var94) (f418994 c424029 c424028)))
|4. (~ (c (f418977 (f418994 c424029 c424028) Var93 Var94) c424028))
|5. (p c424028 c424030)
|6. (po c424029 c424028)
|7. (ec c424030 c424029)
|
|> hyp
=============================
Step 19

? (~ (c (f418977 (f418994 c424029 c424028) c424030 Var94) c424030))

1. (p c424028 c424030)
2. (po c424029 c424028)
3. (ec c424030 c424029)

> ((~ (c (f418977 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 20

? (~ (p (f418994 c424029 c424028) c424030))

1. (c (f418977 (f418994 c424029 c424028) c424030 Var94) c424030)
2. (p c424028 c424030)
3. (po c424029 c424028)
4. (ec c424030 c424029)

> ((~ (p X Y)) <-- (p X Z) (~ (o Y Z)))
|=============================
|Step 21
|
|? (p (f418994 c424029 c424028) c424029)
|
|1. (p (f418994 c424029 c424028) c424030)
|2. (c (f418977 (f418994 c424029 c424028) c424030 Var94) c424030)
|3. (p c424028 c424030)
|4. (po c424029 c424028)
|5. (ec c424030 c424029)
|
|> ((p (f418994 X Y) X) <-- (o X Y))
|=============================
|Step 22
|
|? (o c424029 c424028)
|
|1. (~ (p (f418994 c424029 c424028) c424029))
|2. (p (f418994 c424029 c424028) c424030)
|3. (c (f418977 (f418994 c424029 c424028) c424030 Var94) c424030)
|4. (p c424028 c424030)
|5. (po c424029 c424028)
|6. (ec c424030 c424029)
|
|> ((o X Y) <-- (po X Y))
|=============================
|Step 23
|
|? (po c424029 c424028)
|
|1. (~ (o c424029 c424028))
|2. (~ (p (f418994 c424029 c424028) c424029))
|3. (p (f418994 c424029 c424028) c424030)
|4. (c (f418977 (f418994 c424029 c424028) c424030 Var94) c424030)
|5. (p c424028 c424030)
|6. (po c424029 c424028)
|7. (ec c424030 c424029)
|
|> hyp
=============================
Step 24

? (~ (o c424030 c424029))

1. (p (f418994 c424029 c424028) c424030)
2. (c (f418977 (f418994 c424029 c424028) c424030 Var94) c424030)
3. (p c424028 c424030)
4. (po c424029 c424028)
5. (ec c424030 c424029)

> ((~ (o X Y)) <-- (ec X Y))
=============================
Step 25

? (ec c424030 c424029)

1. (o c424030 c424029)
2. (p (f418994 c424029 c424028) c424030)
3. (c (f418977 (f418994 c424029 c424028) c424030 Var94) c424030)
4. (p c424028 c424030)
5. (po c424029 c424028)
6. (ec c424030 c424029)

> hyp


LEMMA

External connection implies connection.
=============================
Step 1

? (all x (all y ((ec x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (ec c429259 c429258)) v (c c429259 c429258))


> hypdisj
=============================
Step 3

? (c c429259 c429258)

1. (ec c429259 c429258)

> ((c X Y) <-- (ec X Y))
=============================
Step 4

? (ec c429259 c429258)

1. (~ (c c429259 c429258))
2. (ec c429259 c429258)

> hyp


LEMMA

Partial overlap implies overlap.
=============================
Step 1

? (all x (all y ((po x y) => (o x y))))


> revsk
=============================
Step 2

? ((~ (po c434544 c434543)) v (o c434544 c434543))


> hypdisj
=============================
Step 3

? (o c434544 c434543)

1. (po c434544 c434543)

> ((o X Y) <-- (po X Y))
=============================
Step 4

? (po c434544 c434543)

1. (~ (o c434544 c434543))
2. (po c434544 c434543)

> hyp


LEMMA

Overlap implies connection.
=============================
Step 1

? (all x (all y ((o x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (o c439885 c439884)) v (c c439885 c439884))


> hypdisj
=============================
Step 3

? (c c439885 c439884)

1. (o c439885 c439884)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var48 c439884)
|
|1. (~ (c c439885 c439884))
|2. (o c439885 c439884)
|
|> ((p Z X) <-- (~ (c (f434580 Z X Y) Z)))
|=============================
|Step 5
|
|? (~ (c (f434580 Var48 c439884 Var51) Var48))
|
|1. (~ (p Var48 c439884))
|2. (~ (c c439885 c439884))
|3. (o c439885 c439884)
|
|> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
||=============================
||Step 6
||
||? (p (f434597 Var57 Var54) Var54)
||
||1. (c (f434580 (f434597 Var57 Var54) c439884 Var51) (f434597 Var57 Var54))
||2. (~ (p (f434597 Var57 Var54) c439884))
||3. (~ (c c439885 c439884))
||4. (o c439885 c439884)
||
||> ((p (f434597 X Y) Y) <-- (o X Y))
||=============================
||Step 7
||
||? (o Var57 Var54)
||
||1. (~ (p (f434597 Var57 Var54) Var54))
||2. (c (f434580 (f434597 Var57 Var54) c439884 Var51) (f434597 Var57 Var54))
||3. (~ (p (f434597 Var57 Var54) c439884))
||4. (~ (c c439885 c439884))
||5. (o c439885 c439884)
||
||> hyp
|=============================
|Step 8
|
|? (~ (c (f434580 (f434597 c439885 c439884) c439884 Var51) c439884))
|
|1. (c (f434580 (f434597 c439885 c439884) c439884 Var51) (f434597 c439885 c439884))
|2. (~ (p (f434597 c439885 c439884) c439884))
|3. (~ (c c439885 c439884))
|4. (o c439885 c439884)
|
|> ((~ (c (f434580 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 9
|
|? (~ (p (f434597 c439885 c439884) c439884))
|
|1. (c (f434580 (f434597 c439885 c439884) c439884 Var51) c439884)
|2. (c (f434580 (f434597 c439885 c439884) c439884 Var51) (f434597 c439885 c439884))
|3. (~ (p (f434597 c439885 c439884) c439884))
|4. (~ (c c439885 c439884))
|5. (o c439885 c439884)
|
|> hyp
=============================
Step 10

? (c c439885 (f434597 c439885 c439884))

1. (~ (c c439885 c439884))
2. (o c439885 c439884)

> ((c Y X) <-- (c X Y))
=============================
Step 11

? (c (f434597 c439885 c439884) c439885)

1. (~ (c c439885 (f434597 c439885 c439884)))
2. (~ (c c439885 c439884))
3. (o c439885 c439884)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 12
|
|? (p (f434597 c439885 Var71) c439885)
|
|1. (~ (c (f434597 c439885 c439884) c439885))
|2. (~ (c c439885 (f434597 c439885 c439884)))
|3. (~ (c c439885 c439884))
|4. (o c439885 c439884)
|
|> ((p (f434597 X Y) X) <-- (o X Y))
|=============================
|Step 13
|
|? (o c439885 Var71)
|
|1. (~ (p (f434597 c439885 Var71) c439885))
|2. (~ (c (f434597 c439885 c439884) c439885))
|3. (~ (c c439885 (f434597 c439885 c439884)))
|4. (~ (c c439885 c439884))
|5. (o c439885 c439884)
|
|> hyp
=============================
Step 14

? (c (f434597 c439885 c439884) (f434597 c439885 c439884))

1. (~ (c (f434597 c439885 c439884) c439885))
2. (~ (c c439885 (f434597 c439885 c439884)))
3. (~ (c c439885 c439884))
4. (o c439885 c439884)

> ((c X X) <--)


LEMMA

Parthood transports connection from part to whole.
=============================
Step 1

? (all x (all y (all z (((p x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (p c445284 c445283)) v (~ (c c445282 c445284))) v (c c445282 c445283))


> hypdisj
=============================
Step 3

? (c c445282 c445283)

1. (c c445282 c445284)
2. (p c445284 c445283)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var24 c445283)
|
|1. (~ (c c445282 c445283))
|2. (c c445282 c445284)
|3. (p c445284 c445283)
|
|> hyp
=============================
Step 5

? (c c445282 c445284)

1. (~ (c c445282 c445283))
2. (c c445282 c445284)
3. (p c445284 c445283)

> hyp


LEMMA

From ec(x,y) and po(y,z), either x is disconnected from z or connected to z.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (po y z)) => ((dc x z) v (c x z))))))


> revsk
=============================
Step 2

? (((~ (ec c450839 c450838)) v (~ (po c450838 c450837))) v ((dc c450839 c450837) v (c c450839 c450837)))


> hypdisj
=============================
Step 3

? (c c450839 c450837)

1. (~ (dc c450839 c450837))
2. (po c450838 c450837)
3. (ec c450839 c450838)

> ((c X Y) <-- (~ (dc X Y)))
=============================
Step 4

? (~ (dc c450839 c450837))

1. (~ (c c450839 c450837))
2. (~ (dc c450839 c450837))
3. (po c450838 c450837)
4. (ec c450839 c450838)

> hyp


LEMMA

In the connected case, ec(x,z) or po(x,z) or p(x,z).
=============================
Step 1

? (all x (all y (all z ((((ec x y) & (po y z)) & (c x z)) => (((ec x z) v (po x z)) v (p x z))))))


> revsk
=============================
Step 2

? ((((~ (ec c456660 c456659)) v (~ (po c456659 c456658))) v (~ (c c456660 c456658))) v (((ec c456660 c456658) v (po c456660 c456658)) v (p c456660 c456658)))


> hypdisj
=============================
Step 3

? (p c456660 c456658)

1. (~ (po c456660 c456658))
2. (~ (ec c456660 c456658))
3. (c c456660 c456658)
4. (po c456659 c456658)
5. (ec c456660 c456659)

> ((p X Y) <-- (o X Y) (~ (p Y X)) (~ (po X Y)))
||=============================
||Step 4
||
||? (o c456660 c456658)
||
||1. (~ (p c456660 c456658))
||2. (~ (po c456660 c456658))
||3. (~ (ec c456660 c456658))
||4. (c c456660 c456658)
||5. (po c456659 c456658)
||6. (ec c456660 c456659)
||
||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||=============================
|||Step 5
|||
|||? (c c456660 c456658)
|||
|||1. (~ (o c456660 c456658))
|||2. (~ (p c456660 c456658))
|||3. (~ (po c456660 c456658))
|||4. (~ (ec c456660 c456658))
|||5. (c c456660 c456658)
|||6. (po c456659 c456658)
|||7. (ec c456660 c456659)
|||
|||> hyp
||=============================
||Step 6
||
||? (~ (ec c456660 c456658))
||
||1. (~ (o c456660 c456658))
||2. (~ (p c456660 c456658))
||3. (~ (po c456660 c456658))
||4. (~ (ec c456660 c456658))
||5. (c c456660 c456658)
||6. (po c456659 c456658)
||7. (ec c456660 c456659)
||
||> hyp
|=============================
|Step 7
|
|? (~ (p c456658 c456660))
|
|1. (~ (p c456660 c456658))
|2. (~ (po c456660 c456658))
|3. (~ (ec c456660 c456658))
|4. (c c456660 c456658)
|5. (po c456659 c456658)
|6. (ec c456660 c456659)
|
|> ((~ (p Z X)) <-- (ec X Y) (po Y Z))
||=============================
||Step 8
||
||? (ec c456660 Var37)
||
||1. (p c456658 c456660)
||2. (~ (p c456660 c456658))
||3. (~ (po c456660 c456658))
||4. (~ (ec c456660 c456658))
||5. (c c456660 c456658)
||6. (po c456659 c456658)
||7. (ec c456660 c456659)
||
||> hyp
|=============================
|Step 9
|
|? (po c456659 c456658)
|
|1. (p c456658 c456660)
|2. (~ (p c456660 c456658))
|3. (~ (po c456660 c456658))
|4. (~ (ec c456660 c456658))
|5. (c c456660 c456658)
|6. (po c456659 c456658)
|7. (ec c456660 c456659)
|
|> hyp
=============================
Step 10

? (~ (po c456660 c456658))

1. (~ (p c456660 c456658))
2. (~ (po c456660 c456658))
3. (~ (ec c456660 c456658))
4. (c c456660 c456658)
5. (po c456659 c456658)
6. (ec c456660 c456659)

> hyp


LEMMA

Parthood plus failure of converse parthood gives proper part.
=============================
Step 1

? (all x (all y (((p x y) & (~ (p y x))) => (pp x y))))


> revsk
=============================
Step 2

? (((~ (p c463091 c463090)) v (p c463090 c463091)) v (pp c463091 c463090))


> hypdisj
=============================
Step 3

? (pp c463091 c463090)

1. (~ (p c463090 c463091))
2. (p c463091 c463090)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 4
|
|? (p c463091 c463090)
|
|1. (~ (pp c463091 c463090))
|2. (~ (p c463090 c463091))
|3. (p c463091 c463090)
|
|> hyp
=============================
Step 5

? (~ (p c463090 c463091))

1. (~ (pp c463091 c463090))
2. (~ (p c463090 c463091))
3. (p c463091 c463090)

> hyp


LEMMA

Proper part is tangential or non-tangential.
=============================
Step 1

? (all x (all y ((pp x y) => ((tpp x y) v (ntpp x y)))))


> revsk
=============================
Step 2

? ((~ (pp c469673 c469672)) v ((tpp c469673 c469672) v (ntpp c469673 c469672)))


> hypdisj
=============================
Step 3

? (ntpp c469673 c469672)

1. (~ (tpp c469673 c469672))
2. (pp c469673 c469672)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f463202 Z X Y) Z)))
|=============================
|Step 4
|
|? (pp c469673 c469672)
|
|1. (~ (ntpp c469673 c469672))
|2. (~ (tpp c469673 c469672))
|3. (pp c469673 c469672)
|
|> hyp
=============================
Step 5

? (~ (ec (f463202 c469673 c469672 Var32) c469673))

1. (~ (ntpp c469673 c469672))
2. (~ (tpp c469673 c469672))
3. (pp c469673 c469672)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 6
||
||? (pp c469673 Var36)
||
||1. (ec (f463202 c469673 c469672 Var32) c469673)
||2. (~ (ntpp c469673 c469672))
||3. (~ (tpp c469673 c469672))
||4. (pp c469673 c469672)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f463202 c469673 c469672 Var32) c469672)
|
|1. (ec (f463202 c469673 c469672 Var32) c469673)
|2. (~ (ntpp c469673 c469672))
|3. (~ (tpp c469673 c469672))
|4. (pp c469673 c469672)
|
|> ((ec (f463202 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 8
||
||? (~ (ntpp c469673 c469672))
||
||1. (~ (ec (f463202 c469673 c469672 Var32) c469672))
||2. (ec (f463202 c469673 c469672 Var32) c469673)
||3. (~ (ntpp c469673 c469672))
||4. (~ (tpp c469673 c469672))
||5. (pp c469673 c469672)
||
||> hyp
|=============================
|Step 9
|
|? (pp c469673 c469672)
|
|1. (~ (ec (f463202 c469673 c469672 Var32) c469672))
|2. (ec (f463202 c469673 c469672 Var32) c469673)
|3. (~ (ntpp c469673 c469672))
|4. (~ (tpp c469673 c469672))
|5. (pp c469673 c469672)
|
|> hyp
=============================
Step 10

? (~ (tpp c469673 c469672))

1. (ec (f463202 c469673 c469672 Var32) c469673)
2. (~ (ntpp c469673 c469672))
3. (~ (tpp c469673 c469672))
4. (pp c469673 c469672)

> hyp


LEMMA

Split into dc(x,z) or c(x,z). In the connected case use Lemma7. If p(x,z), combine with Lemma1 to get pp(x,z), then Lemma9 gives tpp(x,z) or ntpp(x,z).
=============================
Step 1

? (all x (all y (all z (((ec x y) & (po y z)) => (((((dc x z) v (ec x z)) v (po x z)) v (tpp x z)) v (ntpp x z))))))


> revsk
=============================
Step 2

? (((~ (ec c476408 c476407)) v (~ (po c476407 c476406))) v (((((dc c476408 c476406) v (ec c476408 c476406)) v (po c476408 c476406)) v (tpp c476408 c476406)) v (ntpp c476408 c476406)))


> hypdisj
=============================
Step 3

? (ntpp c476408 c476406)

1. (~ (tpp c476408 c476406))
2. (~ (po c476408 c476406))
3. (~ (ec c476408 c476406))
4. (~ (dc c476408 c476406))
5. (po c476407 c476406)
6. (ec c476408 c476407)

> ((ntpp X Y) <-- (pp X Y) (~ (tpp X Y)))
|=============================
|Step 4
|
|? (pp c476408 c476406)
|
|1. (~ (ntpp c476408 c476406))
|2. (~ (tpp c476408 c476406))
|3. (~ (po c476408 c476406))
|4. (~ (ec c476408 c476406))
|5. (~ (dc c476408 c476406))
|6. (po c476407 c476406)
|7. (ec c476408 c476407)
|
|> ((pp Y X) <-- (p Y X) (~ (p X Y)))
||=============================
||Step 5
||
||? (p c476408 c476406)
||
||1. (~ (pp c476408 c476406))
||2. (~ (ntpp c476408 c476406))
||3. (~ (tpp c476408 c476406))
||4. (~ (po c476408 c476406))
||5. (~ (ec c476408 c476406))
||6. (~ (dc c476408 c476406))
||7. (po c476407 c476406)
||8. (ec c476408 c476407)
||
||> ((p X Y) <-- (o X Y) (~ (p Y X)) (~ (po X Y)))
||||=============================
||||Step 6
||||
||||? (o c476408 c476406)
||||
||||1. (~ (p c476408 c476406))
||||2. (~ (pp c476408 c476406))
||||3. (~ (ntpp c476408 c476406))
||||4. (~ (tpp c476408 c476406))
||||5. (~ (po c476408 c476406))
||||6. (~ (ec c476408 c476406))
||||7. (~ (dc c476408 c476406))
||||8. (po c476407 c476406)
||||9. (ec c476408 c476407)
||||
||||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||||=============================
|||||Step 7
|||||
|||||? (c c476408 c476406)
|||||
|||||1. (~ (o c476408 c476406))
|||||2. (~ (p c476408 c476406))
|||||3. (~ (pp c476408 c476406))
|||||4. (~ (ntpp c476408 c476406))
|||||5. (~ (tpp c476408 c476406))
|||||6. (~ (po c476408 c476406))
|||||7. (~ (ec c476408 c476406))
|||||8. (~ (dc c476408 c476406))
|||||9. (po c476407 c476406)
|||||10. (ec c476408 c476407)
|||||
|||||> ((c X Y) <-- (~ (dc X Y)))
|||||=============================
|||||Step 8
|||||
|||||? (~ (dc c476408 c476406))
|||||
|||||1. (~ (c c476408 c476406))
|||||2. (~ (o c476408 c476406))
|||||3. (~ (p c476408 c476406))
|||||4. (~ (pp c476408 c476406))
|||||5. (~ (ntpp c476408 c476406))
|||||6. (~ (tpp c476408 c476406))
|||||7. (~ (po c476408 c476406))
|||||8. (~ (ec c476408 c476406))
|||||9. (~ (dc c476408 c476406))
|||||10. (po c476407 c476406)
|||||11. (ec c476408 c476407)
|||||
|||||> hyp
||||=============================
||||Step 9
||||
||||? (~ (ec c476408 c476406))
||||
||||1. (~ (o c476408 c476406))
||||2. (~ (p c476408 c476406))
||||3. (~ (pp c476408 c476406))
||||4. (~ (ntpp c476408 c476406))
||||5. (~ (tpp c476408 c476406))
||||6. (~ (po c476408 c476406))
||||7. (~ (ec c476408 c476406))
||||8. (~ (dc c476408 c476406))
||||9. (po c476407 c476406)
||||10. (ec c476408 c476407)
||||
||||> hyp
|||=============================
|||Step 10
|||
|||? (~ (p c476406 c476408))
|||
|||1. (~ (p c476408 c476406))
|||2. (~ (pp c476408 c476406))
|||3. (~ (ntpp c476408 c476406))
|||4. (~ (tpp c476408 c476406))
|||5. (~ (po c476408 c476406))
|||6. (~ (ec c476408 c476406))
|||7. (~ (dc c476408 c476406))
|||8. (po c476407 c476406)
|||9. (ec c476408 c476407)
|||
|||> ((~ (p Z X)) <-- (ec X Y) (po Y Z))
||||=============================
||||Step 11
||||
||||? (ec c476408 Var55)
||||
||||1. (p c476406 c476408)
||||2. (~ (p c476408 c476406))
||||3. (~ (pp c476408 c476406))
||||4. (~ (ntpp c476408 c476406))
||||5. (~ (tpp c476408 c476406))
||||6. (~ (po c476408 c476406))
||||7. (~ (ec c476408 c476406))
||||8. (~ (dc c476408 c476406))
||||9. (po c476407 c476406)
||||10. (ec c476408 c476407)
||||
||||> hyp
|||=============================
|||Step 12
|||
|||? (po c476407 c476406)
|||
|||1. (p c476406 c476408)
|||2. (~ (p c476408 c476406))
|||3. (~ (pp c476408 c476406))
|||4. (~ (ntpp c476408 c476406))
|||5. (~ (tpp c476408 c476406))
|||6. (~ (po c476408 c476406))
|||7. (~ (ec c476408 c476406))
|||8. (~ (dc c476408 c476406))
|||9. (po c476407 c476406)
|||10. (ec c476408 c476407)
|||
|||> hyp
||=============================
||Step 13
||
||? (~ (po c476408 c476406))
||
||1. (~ (p c476408 c476406))
||2. (~ (pp c476408 c476406))
||3. (~ (ntpp c476408 c476406))
||4. (~ (tpp c476408 c476406))
||5. (~ (po c476408 c476406))
||6. (~ (ec c476408 c476406))
||7. (~ (dc c476408 c476406))
||8. (po c476407 c476406)
||9. (ec c476408 c476407)
||
||> hyp
|=============================
|Step 14
|
|? (~ (p c476406 c476408))
|
|1. (~ (pp c476408 c476406))
|2. (~ (ntpp c476408 c476406))
|3. (~ (tpp c476408 c476406))
|4. (~ (po c476408 c476406))
|5. (~ (ec c476408 c476406))
|6. (~ (dc c476408 c476406))
|7. (po c476407 c476406)
|8. (ec c476408 c476407)
|
|> ((~ (p Z X)) <-- (ec X Y) (po Y Z))
||=============================
||Step 15
||
||? (ec c476408 Var61)
||
||1. (p c476406 c476408)
||2. (~ (pp c476408 c476406))
||3. (~ (ntpp c476408 c476406))
||4. (~ (tpp c476408 c476406))
||5. (~ (po c476408 c476406))
||6. (~ (ec c476408 c476406))
||7. (~ (dc c476408 c476406))
||8. (po c476407 c476406)
||9. (ec c476408 c476407)
||
||> hyp
|=============================
|Step 16
|
|? (po c476407 c476406)
|
|1. (p c476406 c476408)
|2. (~ (pp c476408 c476406))
|3. (~ (ntpp c476408 c476406))
|4. (~ (tpp c476408 c476406))
|5. (~ (po c476408 c476406))
|6. (~ (ec c476408 c476406))
|7. (~ (dc c476408 c476406))
|8. (po c476407 c476406)
|9. (ec c476408 c476407)
|
|> hyp
=============================
Step 17

? (~ (tpp c476408 c476406))

1. (~ (ntpp c476408 c476406))
2. (~ (tpp c476408 c476406))
3. (~ (po c476408 c476406))
4. (~ (ec c476408 c476406))
5. (~ (dc c476408 c476406))
6. (po c476407 c476406)
7. (ec c476408 c476407)

> hyp
